\begin{tabbing}
MsgA(${\it ds}$;${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$x$:Id fp$\rightarrow$ ${\it ds}$($x$)?Void\+
\\[0ex]$\times$$a$:Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;locl($a$))$\rightarrow$Prop
\\[0ex]$\times$${\it kx}$:Knd$\times$Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;1of(${\it kx}$))$\rightarrow$${\it ds}$(2of(${\it kx}$))?Void
\\[0ex]$\times$\=${\it kl}$:Knd$\times$IdLnk fp$\rightarrow$\+
\\[0ex](${\it tg}$:Id$\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;1of(${\it kl}$))$\rightarrow$(${\it da}$(rcv(2of(${\it kl}$),${\it tg}$))?Void List))) List
\-\\[0ex]$\times$$x$:Id fp$\rightarrow$ Knd List
\\[0ex]$\times$${\it ltg}$:IdLnk$\times$Id fp$\rightarrow$ Knd List
\\[0ex]$\times$$k$:Knd fp$\rightarrow$ Id List
\\[0ex]$\times$$k$:Knd fp$\rightarrow$ IdLnk List
\\[0ex]$\times$${\it ltg}$:Id fp$\rightarrow$ Knd List
\\[0ex]$\times$Top
\-
\end{tabbing}